/**
 * Developed by PuzzleDev s.n.c.
 * 2012 all rights reserved.
 * www.puzzledev.com
 */
package it.polimi.nuzot.ltl

import org.junit._
import Assert._
import it.polimi.nuzot.shell.ShellInterpreter
import it.polimi.nuzot.smt.grammar._
import it.polimi.nuzot.Z3.Z3Interpreter
import it.polimi.nuzot.shell.ShellParser
import it.polimi.nuzot.smt.TypeChecker


/**
 * @author Michele Sama (m.sama@puzzledev.com)
 * 
 * TestCase for the LTLInterpreter
 */
class LTLInterpreterTestCase {

    
    val interpreter = new LTLInterpreter()
    
    @Before
    def setUp = {
        interpreter.temporalExt = 5
    }
    
    @Test
    def testDeneg_NotNot() = {
        assertEquals(Term.True, interpreter.deneg(Not(Not(Term.True))))
    }
    
    @Test
    def testDeneg_NotAnd() = {
        assertEquals(Or(Term.False, Term.False),
                interpreter.deneg(Not(And(Term.True, Term.True)))
                )
    }
    
    @Test
    def testDeneg_NotOr() = {
        assertEquals(And(Term.False, Term.False),
                interpreter.deneg(Not(Or(Term.True, Term.True)))
                )
    }
    
    
    /**
     * Assert the correct expansion of LTL function
     * in a working environment.
     * 
     * <p>This could be considered an integration test
     * because it not only checks the current expansion
     * of a single operator but it also checks its
     * evaluation (e.g. its satisfiability)
     */
    def assertExecution(input: String, expected: String) = {
        val parser = new ShellParser()
        val inputScript = parser.parseAll(
		                parser.script, input)
		                .getOrElse(null)
		
		// Recreates a complete execution stack
		val z3 = new Z3Interpreter()
        val typeChecker = new TypeChecker()
        typeChecker.next(z3)
		val ltl = new LTLInterpreter()
    	ltl.next(typeChecker)
    	ltl.temporalExt = 5
		val shell = new ShellInterpreter()
        shell.next(ltl)
    			
        shell.doVisitPreconditions(Script(List())) ++ 
        		shell.doVisit(inputScript)
        assertEquals(input, shell.precomputed.toString())
        assertEquals(input, ltl.precomputed.toString())
        assertEquals(expected, z3.precomputed.toString())
        assertTrue(z3.checkSat())
    }
    
    @Test
    def testTemporalAssert() = {
        val input = 
            	"(declare-tfun x () Bool)\n" +
        		"(assert-t x 2)\n" +
        		"(assert-t (! x) 4)" 

        val expected = 
            	"(declare-fun iLoop () Int)\n" +
				"(declare-fun loopex () Bool)\n" +
				"(assert (or (! loopex) (and (< 0 iLoop) (<= iLoop 5))))\n" +
				"(declare-fun x (Int) Bool)\n" +
				"(assert (x 2))\n" +
				"(assert (and loopex (iff (x (- iLoop 1)) (x 5))))\n" +
				"(declare-fun zot-p0 (Int) Bool)\n" +
				"(assert (zot-p0 4))\n" +
				"(assert (iff (zot-p0 0) (! (x 0))))\n" +
				"(assert (iff (zot-p0 1) (! (x 1))))\n" +
				"(assert (iff (zot-p0 2) (! (x 2))))\n" +
				"(assert (iff (zot-p0 3) (! (x 3))))\n" +
				"(assert (iff (zot-p0 4) (! (x 4))))\n" +
				"(assert (iff (zot-p0 5) (! (x 5))))\n" +
				"(assert (iff (zot-p0 6) (! (x 6))))\n" +
				"(assert (and loopex (iff (x (- iLoop 1)) (x 5))))"
        
        assertExecution(input, expected)
    }
    
    @Test
    def testVisitPreconditions() = {
        val outputScript = interpreter.visitPreconditions(Script(List()))
        val expected = 
            	"(declare-fun iLoop () Int)\n" +
     			"(declare-fun loopex () Bool)\n" +
     			"(assert (or (! loopex) (and (< 0 iLoop) (<= iLoop 5))))"
        
        assertEquals(expected, outputScript.toString())
    }
    
    @Test
    def testDeclareTFun() = {
        val input = "(declare-tfun x () Bool)"
        val expected = 
            "(declare-fun iLoop () Int)\n" +
            "(declare-fun loopex () Bool)\n" +
     		"(assert (or (! loopex) (and (< 0 iLoop) (<= iLoop 5))))\n" +
     		"(declare-fun x (Int) Bool)"
        
        assertExecution(input, expected)
    }
    
    @Test
    def testNext() = {
        val input = 
            	"(declare-tfun x () Bool)\n" +
        		"(assert (next x))"

        val expected = "(declare-fun iLoop () Int)\n" +
     			"(declare-fun loopex () Bool)\n" +
     			"(assert (or (! loopex) (and (< 0 iLoop) (<= iLoop 5))))\n" +
     			"(declare-fun x (Int) Bool)\n" +
     			"(declare-fun zot-p0 (Int) Bool)\n" +
     			"(assert (zot-p0 1))\n" +
     			"(assert (iff (zot-p0 0) (x 1)))\n" +
     			"(assert (iff (zot-p0 1) (x 2)))\n" +
     			"(assert (iff (zot-p0 2) (x 3)))\n" +
     			"(assert (iff (zot-p0 3) (x 4)))\n" +
     			"(assert (iff (zot-p0 4) (x 5)))\n" +
     			"(assert (iff (zot-p0 5) (x 6)))\n" +
     			"(assert (and loopex (iff (x (- iLoop 1)) (x 5))))"
     	 assertExecution(input, expected)
    }
    
    @Test
    def testYesterday() = {
        val input = 
            	"(declare-tfun x () Bool)\n" +
        		"(assert (yesterday x))"

        val expected = "(declare-fun iLoop () Int)\n" +
     			"(declare-fun loopex () Bool)\n" +
     			"(assert (or (! loopex) (and (< 0 iLoop) (<= iLoop 5))))\n" +
     			"(declare-fun x (Int) Bool)\n" +
     			"(declare-fun zot-p0 (Int) Bool)\n" +
     			"(assert (zot-p0 1))\n" +
     			"(assert (iff (zot-p0 1) (x 0)))\n" +
     			"(assert (iff (zot-p0 2) (x 1)))\n" +
     			"(assert (iff (zot-p0 3) (x 2)))\n" +
     			"(assert (iff (zot-p0 4) (x 3)))\n" +
     			"(assert (iff (zot-p0 5) (x 4)))\n" +
     			"(assert (iff (zot-p0 6) (x 5)))\n" +
     			"(assert (and loopex (iff (x (- iLoop 1)) (x 5))))"
     	assertExecution(input, expected)
    }
    
    @Test
    def testNot() = {
        val input =
            	"(declare-tfun x () Bool)\n" +
        		"(assert (! x))"
        
        val expected = 
            	"(declare-fun iLoop () Int)\n" +
     			"(declare-fun loopex () Bool)\n" +
     			"(assert (or (! loopex) (and (< 0 iLoop) (<= iLoop 5))))\n" +
     			"(declare-fun x (Int) Bool)\n" +
     			"(declare-fun zot-p0 (Int) Bool)\n" +
     			"(assert (zot-p0 1))\n" +
     			"(assert (iff (zot-p0 0) (! (x 0))))\n" +
     			"(assert (iff (zot-p0 1) (! (x 1))))\n" +
     			"(assert (iff (zot-p0 2) (! (x 2))))\n" +
     			"(assert (iff (zot-p0 3) (! (x 3))))\n" +
     			"(assert (iff (zot-p0 4) (! (x 4))))\n" +
     			"(assert (iff (zot-p0 5) (! (x 5))))\n" +
     			"(assert (iff (zot-p0 6) (! (x 6))))\n" +
     			"(assert (and loopex (iff (x (- iLoop 1)) (x 5))))"
     	
     	assertExecution(input, expected)
    }
    
    @Test
    def testAnd() = {
        val input = 
            	"(declare-tfun x () Bool)\n" +
        		"(declare-tfun y () Bool)\n" +
        		"(assert (and x y))"
        
        val expected = "(declare-fun iLoop () Int)\n" +
     			"(declare-fun loopex () Bool)\n" +
     			"(assert (or (! loopex) (and (< 0 iLoop) (<= iLoop 5))))\n" +
     			"(declare-fun x (Int) Bool)\n" +
     			"(declare-fun y (Int) Bool)\n" +
     			"(declare-fun zot-p0 (Int) Bool)\n" +
     			"(assert (zot-p0 1))\n" +
     			"(assert (iff (zot-p0 0) (and (x 0) (y 0))))\n" +
     			"(assert (iff (zot-p0 1) (and (x 1) (y 1))))\n" +
     			"(assert (iff (zot-p0 2) (and (x 2) (y 2))))\n" +
     			"(assert (iff (zot-p0 3) (and (x 3) (y 3))))\n" +
     			"(assert (iff (zot-p0 4) (and (x 4) (y 4))))\n" +
     			"(assert (iff (zot-p0 5) (and (x 5) (y 5))))\n" +
     			"(assert (iff (zot-p0 6) (and (x 6) (y 6))))\n" +
     			"(assert (and loopex (iff (x (- iLoop 1)) (x 5))))\n" +
     			"(assert (and loopex (iff (y (- iLoop 1)) (y 5))))"
     	assertExecution(input, expected)
    }
    
    @Test
    def testOr() = {
        val input = 
            	"(declare-tfun x () Bool)\n" +
        		"(declare-tfun y () Bool)\n" +
        		"(assert (or x y))"
        
        val expected = "(declare-fun iLoop () Int)\n" +
     			"(declare-fun loopex () Bool)\n" +
     			"(assert (or (! loopex) (and (< 0 iLoop) (<= iLoop 5))))\n" +
     			"(declare-fun x (Int) Bool)\n" +
     			"(declare-fun y (Int) Bool)\n" +
     			"(declare-fun zot-p0 (Int) Bool)\n" +
     			"(assert (zot-p0 1))\n" +
     			"(assert (iff (zot-p0 0) (or (x 0) (y 0))))\n" +
     			"(assert (iff (zot-p0 1) (or (x 1) (y 1))))\n" +
     			"(assert (iff (zot-p0 2) (or (x 2) (y 2))))\n" +
     			"(assert (iff (zot-p0 3) (or (x 3) (y 3))))\n" +
     			"(assert (iff (zot-p0 4) (or (x 4) (y 4))))\n" +
     			"(assert (iff (zot-p0 5) (or (x 5) (y 5))))\n" +
     			"(assert (iff (zot-p0 6) (or (x 6) (y 6))))\n" +
     			"(assert (and loopex (iff (x (- iLoop 1)) (x 5))))\n" +
     			"(assert (and loopex (iff (y (- iLoop 1)) (y 5))))"
     			
     	 assertExecution(input, expected)
    }
    
    @Test
    def testUntil() = {
        val input =
            	"(declare-tfun x () Bool)\n" +
        		"(declare-tfun y () Bool)\n" +
        		"(assert (until x y))"
        
        val expected = "(declare-fun iLoop () Int)\n" +
     			"(declare-fun loopex () Bool)\n" +
     			"(assert (or (! loopex) (and (< 0 iLoop) (<= iLoop 5))))\n" +
     			"(declare-fun x (Int) Bool)\n" +
     			"(declare-fun y (Int) Bool)\n" +
     			"(declare-fun zot-p0 (Int) Bool)\n" +
     			"(assert (zot-p0 1))\n" +
     			"(assert (iff (zot-p0 0) (or (y 0) (and (x 0) (zot-p0 1)))))\n" +
     			"(assert (iff (zot-p0 1) (or (y 1) (and (x 1) (zot-p0 2)))))\n" +
     			"(assert (iff (zot-p0 2) (or (y 2) (and (x 2) (zot-p0 3)))))\n" +
     			"(assert (iff (zot-p0 3) (or (y 3) (and (x 3) (zot-p0 4)))))\n" +
     			"(assert (iff (zot-p0 4) (or (y 4) (and (x 4) (zot-p0 5)))))\n" +
     			"(assert (iff (zot-p0 5) (or (y 5) (and (x 5) (zot-p0 6)))))\n" +
     			"(assert (and loopex (iff (x (- iLoop 1)) (x 5))))\n" +
     			"(assert (and loopex (iff (y (- iLoop 1)) (y 5))))\n" +
     			"(assert (-> loopex (iff (zot-p0 6) (zot-p0 iLoop)))\n" + // TODO for everyone
     			"(assert (-> (! loopex) (! (zot-p0 6)))\n" +
     			"(declare-fun i_eve_zot-p0 () Int)\n" +
     			"(assert (-> loopex (-> (zot-p0 5) (and (<= loop i_eve_zot-p0) (<= i_eve_zot-p0 5) (zot-p0 i_eve_zot-p0)))))"
     	
     	assertExecution(input, expected)
    }
    
    @Test
    def testRelease() = {
        val input =
            	"(declare-tfun x () Bool)\n" +
        		"(declare-tfun y () Bool)\n" +
        		"(assert (release x y))"
        
        val expected = "(declare-fun iLoop () Int)\n" +
     			"(declare-fun loopex () Bool)\n" +
     			"(assert (or (! loopex) (and (< 0 iLoop) (<= iLoop 5))))\n" +
     			"(declare-fun x (Int) Bool)\n" +
     			"(declare-fun y (Int) Bool)\n" +
     			"(declare-fun zot-p0 (Int) Bool)\n" +
     			"(assert (zot-p0 1))\n" +
     			"(assert (iff (zot-p0 0) (and (y 0) (or (x 0) (zot-p0 1)))))\n" +
     			"(assert (iff (zot-p0 1) (and (y 1) (or (x 1) (zot-p0 2)))))\n" +
     			"(assert (iff (zot-p0 2) (and (y 2) (or (x 2) (zot-p0 3)))))\n" +
     			"(assert (iff (zot-p0 3) (and (y 3) (or (x 3) (zot-p0 4)))))\n" +
     			"(assert (iff (zot-p0 4) (and (y 4) (or (x 4) (zot-p0 5)))))\n" +
     			"(assert (iff (zot-p0 5) (and (y 5) (or (x 5) (zot-p0 6)))))\n" +
     			"(assert (and loopex (iff (x (- iLoop 1)) (x 5))))\n" +
     			"(assert (and loopex (iff (y (- iLoop 1)) (y 5))))\n" +
     			"(declare-fun i_eve_zot-p0 () Int)\n" +
     			"(assert (-> loopex (-> (! (zot-p0 5)) (and (<= loop i_eve_zot-p0) (<= i_eve_zot-p0 5) (! (zot-p0 i_eve_zot-p0))))))"
     	
     	assertExecution(input, expected)
    }
    
    @Test
    def testSince() = {
        val input =
            	"(declare-tfun x () Bool)\n" +
        		"(declare-tfun y () Bool)\n" +
        		"(assert (since x y))"

        val expected = "(declare-fun iLoop () Int)\n" +
     			"(declare-fun loopex () Bool)\n" +
     			"(assert (or (! loopex) (and (< 0 iLoop) (<= iLoop 5))))\n" +
     			"(declare-fun x (Int) Bool)\n" +
     			"(declare-fun y (Int) Bool)\n" +
     			"(declare-fun zot-p0 (Int) Bool)\n" +
     			"(assert (zot-p0 1))\n" +
     			"(assert (iff (zot-p0 0) (y 0)))\n" +
     			"(assert (iff (zot-p0 1) (or (y 1) (and (x 1) (zot-p0 0)))))\n" +
				"(assert (iff (zot-p0 2) (or (y 2) (and (x 2) (zot-p0 1)))))\n" +
				"(assert (iff (zot-p0 3) (or (y 3) (and (x 3) (zot-p0 2)))))\n" +
				"(assert (iff (zot-p0 4) (or (y 4) (and (x 4) (zot-p0 3)))))\n" +
				"(assert (iff (zot-p0 5) (or (y 5) (and (x 5) (zot-p0 4)))))\n" +
				"(assert (iff (zot-p0 6) (or (y 6) (and (x 6) (zot-p0 5)))))\n" +
				"(assert (and loopex (iff (x (- iLoop 1)) (x 5))))\n" +
     			"(assert (and loopex (iff (y (- iLoop 1)) (y 5))))"
     	assertExecution(input, expected)
    }
    
    @Test
    def testTrigger() = {
        val input =
            	"(declare-tfun x () Bool)\n" +
        		"(declare-tfun y () Bool)\n" +
        		"(assert (trigger x y))"
        
        val expected = "(declare-fun iLoop () Int)\n" +
     			"(declare-fun loopex () Bool)\n" +
     			"(assert (or (! loopex) (and (< 0 iLoop) (<= iLoop 5))))\n" +
     			"(declare-fun x (Int) Bool)\n" +
     			"(declare-fun y (Int) Bool)\n" +
     			"(declare-fun zot-p0 (Int) Bool)\n" +
     			"(assert (zot-p0 1))\n" +
     			"(assert (iff (zot-p0 0) (y 0)))\n" +
     			"(assert (iff (zot-p0 1) (and (y 1) (or (x 1) (zot-p0 0)))))\n" +
				"(assert (iff (zot-p0 2) (and (y 2) (or (x 2) (zot-p0 1)))))\n" +
				"(assert (iff (zot-p0 3) (and (y 3) (or (x 3) (zot-p0 2)))))\n" +
				"(assert (iff (zot-p0 4) (and (y 4) (or (x 4) (zot-p0 3)))))\n" +
				"(assert (iff (zot-p0 5) (and (y 5) (or (x 5) (zot-p0 4)))))\n" +
				"(assert (iff (zot-p0 6) (and (y 6) (or (x 6) (zot-p0 5)))))\n" +
				"(assert (and loopex (iff (x (- iLoop 1)) (x 5))))\n" +
     			"(assert (and loopex (iff (y (- iLoop 1)) (y 5))))"

     	assertExecution(input, expected)
    }
    
    
}